eq_seq(eq)(s1,s2)
== let k1,g1 = s1
== in
== let k2,g2 = s2 in (k1 = k2)  primrec(k1;tt;i,b. (eq(g1(i),g2(i)))  b) 

latex

Definitions	let x,y = A in B(x;y), (i = j), primrec(n;b;c), tt, x.A(x), p  q, f(a)
FDL editor aliases	eq_seq